package edu.uic.cs.cs582.process.impl;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.Comparator;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.TreeSet;
import java.util.concurrent.atomic.AtomicInteger;

import org.apache.commons.collections.primitives.ArrayIntList;
import org.apache.commons.collections.primitives.IntList;
import org.apache.commons.lang.StringUtils;
import org.apache.log4j.Logger;

import edu.mit.jwi.item.POS;
import edu.uic.cs.cs582.data.Component;
import edu.uic.cs.cs582.data.Polarity;
import edu.uic.cs.cs582.data.Synset;
import edu.uic.cs.cs582.data.Word;
import edu.uic.cs.cs582.misc.Assert;
import edu.uic.cs.cs582.misc.LogHelper;
import edu.uic.cs.cs582.process.CnfGenerator;

public class AddingFrequencyCnfGeneratorImpl extends
		AbstractVariablesOperations implements CnfGenerator
{
	private static final Logger LOGGER = LogHelper
			.getLogger(AddingFrequencyCnfGeneratorImpl.class);

	private static class Variables
	{
		private IntList finalFrequencySummationDigits;
		private Map<Integer, MiddleVariableExpression> allMiddleVariableExpression;

		private Variables(
				IntList finalFrequencySummationDigits,
				Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
		{
			this.finalFrequencySummationDigits = finalFrequencySummationDigits;
			this.allMiddleVariableExpression = allMiddleVariableExpression;
		}
	}

	//	private HashSet<Integer> allFreuqencyVariables = null;

	public AddingFrequencyCnfGeneratorImpl(Component component)
	{
		super(component);
	}

	@Override
	public Set<int[]> generateCnfs(POS pos, Word word, Polarity polarity)
	{
		if (LOGGER.isDebugEnabled())
		{
			LOGGER.debug(LogHelper.LOG_LAYER_ONE_BEGIN + "Process word: "
					+ word + " " + polarity);
		}

		//		allFreuqencyVariables = new HashSet<Integer>();

		Set<int[]> result = new TreeSet<int[]>(new IntArrayComparator());
		int halfFrequencySum = word.getFrequencySum() / 2;

		AtomicInteger variableIndexBase = new AtomicInteger(0);
		if (polarity != Polarity.NEUTRAL)
		{
			Variables variables = generateAndStoreCnfsForNonNeutralWord(word,
					polarity, variableIndexBase, result);
			IntList finalFrequencySummationDigits = variables.finalFrequencySummationDigits;

			Collection<int[]> greaterThanHalfExpression = generateCnfForSummationGreaterThanValue(
					finalFrequencySummationDigits, halfFrequencySum);

			Collection<int[]> greaterThanHalfExpressionEliminatedMiddleVariables = replaceAllMiddleVariables(
					greaterThanHalfExpression,
					variables.allMiddleVariableExpression);

			result.addAll(greaterThanHalfExpressionEliminatedMiddleVariables);
		}
		else
		{
			Variables positiveVariables = generateAndStoreCnfsForNonNeutralWord(
					word, Polarity.POSITIVE, variableIndexBase, result);
			IntList finalPositiveFrequencySummationDigits = positiveVariables.finalFrequencySummationDigits;

			Variables negativeVariables = generateAndStoreCnfsForNonNeutralWord(
					word, Polarity.NEGATIVE, variableIndexBase, result); // continue using variableIndexBase
			IntList finalNegativeFrequencySummationDigits = negativeVariables.finalFrequencySummationDigits;

			Collection<int[]> positiveLessThanOrEqualsToHalfExpression = generateCnfForSummationLessThanOrEqualsToValue(
					finalPositiveFrequencySummationDigits, halfFrequencySum);
			Collection<int[]> negativeLessThanOrEqualsToHalfExpression = generateCnfForSummationLessThanOrEqualsToValue(
					finalNegativeFrequencySummationDigits, halfFrequencySum);

			Collection<int[]> positiveLessThanOrEqualsToHalfExpressionEliminatedMiddleVariables = replaceAllMiddleVariables(
					positiveLessThanOrEqualsToHalfExpression,
					positiveVariables.allMiddleVariableExpression);
			Collection<int[]> negativeLessThanOrEqualsToHalfExpressionEliminatedMiddleVariables = replaceAllMiddleVariables(
					negativeLessThanOrEqualsToHalfExpression,
					negativeVariables.allMiddleVariableExpression);

			result.addAll(positiveLessThanOrEqualsToHalfExpressionEliminatedMiddleVariables);
			result.addAll(negativeLessThanOrEqualsToHalfExpressionEliminatedMiddleVariables);
		}

		//		allFreuqencyVariables.clear();
		//		allFreuqencyVariables = null;

		if (LOGGER.isDebugEnabled())
		{
			LOGGER.debug(LogHelper.LOG_LAYER_ONE_END + "Process word: " + word
					+ " " + polarity);
		}

		return result;
	}

	private Collection<int[]> replaceAllMiddleVariables(
			Collection<int[]> finalExpressionInCnf,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		if (LOGGER.isDebugEnabled())
		{
			LOGGER.debug(LogHelper.LOG_LAYER_TWO_BEGIN
					+ "replaceAllMiddleVariables()");
		}

		TreeSet<int[]> result = new TreeSet<int[]>(new IntArrayComparator());

		recursiveReplaceAndConvert(finalExpressionInCnf,
				allMiddleVariableExpression, result);

		if (LOGGER.isDebugEnabled())
		{
			LOGGER.debug(LogHelper.LOG_LAYER_TWO_END
					+ "replaceAllMiddleVariables()");
		}

		return result;
	}

	private void recursiveReplaceAndConvert(Collection<int[]> expressionInCnf,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression,
			TreeSet<int[]> result)
	{
		for (int[] eachClauseWhichIsInDnf : expressionInCnf)
		{

			List<int[]> replacedClauseInDnf = replaceMiddleVariables(
					eachClauseWhichIsInDnf, allMiddleVariableExpression);

			if (replacedClauseInDnf != null)
			{
				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug(LogHelper.LOG_LAYER_THREE_BEGIN
							+ "convertDnfToCnf()");
				}

				List<int[]> replacedClauseInCnf = convertDnfToCnf(replacedClauseInDnf);

				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug(LogHelper.LOG_LAYER_THREE_END
							+ "replaceMiddleVariables(), and about to do next recursion. ");
				}

				recursiveReplaceAndConvert(replacedClauseInCnf,
						allMiddleVariableExpression, result);
			}
			else
			// nothing replaced, means the original eachClauseWhichIsInDnf is simplest one
			{
				result.add(eachClauseWhichIsInDnf);
				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug(LogHelper.LOG_LAYER_THREE
							+ Arrays.toString(eachClauseWhichIsInDnf)
							+ " is the simplest clause. ");
				}
			}
		}
	}

	private List<int[]> replaceMiddleVariables(int[] eachClauseWhichIsInDnf,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		if (LOGGER.isDebugEnabled())
		{
			LOGGER.debug(LogHelper.LOG_LAYER_THREE_BEGIN
					+ "replaceMiddleVariables() "
					+ Arrays.toString(eachClauseWhichIsInDnf));
		}

		List<int[]> result = new ArrayList<int[]>();

		boolean replaced = false;
		for (int variable : eachClauseWhichIsInDnf)
		{
			Integer variableWithNoSymbol = Integer.valueOf(Math.abs(variable)); // only +variables stored
			MiddleVariableExpression middleVariableExpression = allMiddleVariableExpression
					.get(variableWithNoSymbol);

			// It is not a middle variable
			if (middleVariableExpression == null)
			{
				Assert.isTrue(
						component
								.getSynsetIndexByFrequencySymbol(variableWithNoSymbol) != null,
						"Variable["
								+ variableWithNoSymbol
								+ "] must be initial-frequency variable, since there is no middle variable to match. ");

				result.add(new int[] { variable });
				continue;
			}
			////////////////////////////////////////////////////////////////////

			// there's middle variable, replace it
			List<int[]> replacedExpressionInDnf = null;
			if (variable > 0)
			{
				replacedExpressionInDnf = middleVariableExpression
						.getExpressionInDnf();
			}
			else
			{
				replacedExpressionInDnf = middleVariableExpression
						.getNotExpressionInDnf();
			}

			result.addAll(replacedExpressionInDnf);

			replaced = true;
		}

		if (LOGGER.isDebugEnabled())
		{
			LOGGER.debug(LogHelper.LOG_LAYER_THREE_END
					+ "replaceMiddleVariables() "
					+ Arrays.toString(eachClauseWhichIsInDnf));
		}

		return replaced ? result : null;
	}

	private Variables generateAndStoreCnfsForNonNeutralWord(Word word,
			Polarity polarity, AtomicInteger variableIndexBase,
			Set<int[]> result)
	{
		int initialIndexBase = variableIndexBase.get();
		// stores all the frequency-digit variables for each synset of current word
		LinkedList<IntList> frequencyDigits = new LinkedList<IntList>();

		int wordIndexInComponent = component.getIndexOfWord(word);
		for (Entry<Synset, Integer> frequencyBySynset : word
				.getFrequenciesBySynsetRelateTo().entrySet())
		{
			Synset synset = frequencyBySynset.getKey();
			int frequency = frequencyBySynset.getValue();
			// NOTICE! reverse order!
			String frequencyBinaryString = StringUtils.reverse(Integer
					.toBinaryString(frequency));

			Collection<int[]> cnfForOneFrequency = generateCnfForOneNonNeutralFrequency(
					polarity, synset, frequencyBinaryString,
					variableIndexBase.get(), wordIndexInComponent,
					frequencyDigits);
			result.addAll(cnfForOneFrequency);

			variableIndexBase.addAndGet(frequencyBinaryString.length());
		}

		Assert.isTrue(word.getTotalFrequencyDigitNumber() == (variableIndexBase
				.get() - initialIndexBase));
		// step 4
		Map<Integer, MiddleVariableExpression> allMiddleVariableExpression = generateAndStoreMiddleVariablesExpressions(
				frequencyDigits, word, variableIndexBase);

		Assert.isTrue(frequencyDigits.size() == 1);
		// step 5
		IntList finalFrequencySummationDigits = frequencyDigits.poll();
		Assert.isTrue(finalFrequencySummationDigits.size() >= Integer
				.toBinaryString(word.getFrequencySum()).length());

		return new Variables(finalFrequencySummationDigits,
				allMiddleVariableExpression);
	}

	/**
	 * 
	 *  -------------------------
	 * |Step 2 and 3 in my report|
	 *  -------------------------
	 *  
	 *
	 * Suppose w1 is POSITIVE 
	 * and one synset s1’s frequency is 6 = (110)_bin.
	 *
	 *	   (s1+ -> (x12=1) AND (x11=1) AND (x10=0))
	 * AND (¬s1+ -> (x12=0) AND (x11=0) AND (x10=0)
	 * 	
	 * ⇔      (¬s1+ OR (x12 AND x11 AND ¬x10))
	 * AND (s1+ OR (¬x12 AND ¬x11 AND ¬x10))
	 * 
	 * ⇔      (¬s1+ OR ¬x10)
	 * AND (¬s1+ OR x11)
	 * AND (¬s1+ OR x12)
	 * 
	 * AND (s1+ OR ¬x10)
	 * AND (s1+ OR ¬x11) 
	 * AND (s1+ OR ¬x12)
	 * 
	 * ⇔      (¬s1+ OR ¬x10)
	 * AND (s1+ OR ¬x10)
	 * 
	 * AND (¬s1+ OR x11)
	 * AND (s1+ OR ¬x11) 
	 * 
	 * AND (¬s1+ OR x12)
	 * AND (s1+ OR ¬x12)
	 * 
	 */
	private List<int[]> generateCnfForOneNonNeutralFrequency(
			Polarity wordPolarity, Synset synset, String frequencyBinaryString,
			int variableIndexBase, int wordIndexInComponent,
			List<IntList> frequencyDigits)
	{
		int indexOfSynsetInTheComponent = component.getIndexOfSynset(synset);

		List<int[]> result = new ArrayList<int[]>(
				frequencyBinaryString.length());

		////////////////////////////////////////////////////////////////////////
		// store all the indices for each digit of a frequency for current word 
		IntList frequencyDigitIndices = new ArrayIntList(
				frequencyBinaryString.length());
		// put the frequency digits for one synset of a current word
		frequencyDigits.add(frequencyDigitIndices);
		////////////////////////////////////////////////////////////////////////

		// s1+
		int synsetIndexSymbol = polarSymbol(wordPolarity,
				indexOfSynsetInTheComponent);
		// ¬s1+
		int synsetNotIndexSymbol = not(synsetIndexSymbol);
		int length = frequencyBinaryString.length() + variableIndexBase;
		int[] clause = null;
		for (int variableIndex = variableIndexBase; variableIndex < length; variableIndex++)
		{

			// x11
			int frequencyDigitVariableSymbol = frequencyDigitSymbol(
					variableIndex, wordIndexInComponent);
			// record it for assertion
			component.addRelationBetweenFrequencySymbolAndSynset(
					Integer.valueOf(frequencyDigitVariableSymbol),
					indexOfSynsetInTheComponent);

			// store this digit ////////////////////////////////////////////////
			frequencyDigitIndices.add(frequencyDigitVariableSymbol);
			////////////////////////////////////////////////////////////////////

			// ¬x11
			int frequencyDigitVariableSymbolNotSymbol = not(frequencyDigitVariableSymbol);

			//  (¬s1+ OR ¬x10)
			if (frequencyBinaryString.charAt(variableIndex - variableIndexBase) == '0')
			{
				clause = generateSynsetORVariableClause(synsetNotIndexSymbol,
						frequencyDigitVariableSymbolNotSymbol);
				result.add(clause);
			}
			// (¬s1+ OR x11)
			else
			{
				clause = generateSynsetORVariableClause(synsetNotIndexSymbol,
						frequencyDigitVariableSymbol);
				result.add(clause);
			}

			// (s1+ OR ¬x10) || (s1+ OR ¬x11) 
			clause = generateSynsetORVariableClause(synsetIndexSymbol,
					frequencyDigitVariableSymbolNotSymbol);
			result.add(clause);

		}

		return result;
	}

	private int[] generateSynsetORVariableClause(int synsetIndexSymbol,
			int variableSymbol)
	{
		int[] clause = new int[2];

		// Remember in sorted order
		if (variableSymbol > synsetIndexSymbol)
		{
			clause[0] = synsetIndexSymbol;
			clause[1] = variableSymbol;
		}
		else
		{
			clause[0] = variableSymbol;
			clause[1] = synsetIndexSymbol;
		}

		return clause;
	}

	////////////////////////////////////////////////////////////////////////////

	/**
	 *  -------------------
	 * |Step 4 in my report|
	 *  -------------------
	 *  
	 * @param frequencyDigitsQueue initially it stores digit variables for each frequency
	 * @param nextDigitIndex index for the next generating variable,
	 *  which may be carrier or summation digit
	 * @return
	 */
	private Map<Integer, MiddleVariableExpression> generateAndStoreMiddleVariablesExpressions(
			LinkedList<IntList> frequencyDigitsQueue, Word word,
			AtomicInteger nextDigitIndex)
	{
		// ordered by size in order to let those two with same size process first, 
		// and hence reduce the number of variables. e.g.,
		//     abc : def = 3; hijk : lmno = 4; 3 : 4 = 4 ; total = 3+4+4 = 11
		// BUT, abc : hijk = 4;  def: lmno = 4; 4 : 4 = 4; total = 4+4+4 = 12
		Comparator<IntList> queueSizeSorter = new Comparator<IntList>()
		{
			@Override
			public int compare(IntList o1, IntList o2)
			{
				// order by size
				return o1.size() - o2.size();
			}
		};
		Collections.sort(frequencyDigitsQueue, queueSizeSorter);
		////////////////////////////////////////////////////////////////////////

		int wordIndex = component.getIndexOfWord(word);

		/**
		 * 					x_i+1	x_i	...	x_1	x_0
		 * 			y_i+2	y_i+1	y_i	...	y_1	y_0
		 * ----------------------------------------
		 * c_i+3	c_i+2	c_i+1	c_i	...	c_1	 /
		 * s_i+3	s_i+2	s_i+1	s_i	...	s_1	s_0
		 */
		//		TreeSet<int[]> result = new TreeSet<int[]>(new IntArrayComparator());
		Map<Integer, MiddleVariableExpression> allMiddleVariableExpressions = new HashMap<Integer, MiddleVariableExpression>();

		IntList first = null;
		IntList second = null;
		while ((first = frequencyDigitsQueue.poll()) != null)
		{
			if ((second = frequencyDigitsQueue.poll()) == null)
			{
				// first is the last final one in the queue
				// put it back into the queue for step 5's usage
				frequencyDigitsQueue.offer(first);
				break;
			}

			Assert.isTrue(!first.isEmpty());
			Assert.isTrue(!second.isEmpty());

			IntList frequencySummationDigits = new ArrayIntList(
					second.size() + 1);

			// second's size always >= first since they have been sorted
			// For carries: 	  1, 2, 3, ..., sizeOfFirst ~ total sizeOfFirst
			// For summations: 0, 1, 2, 3, ..., ..., ..., sizeOfSecond ~ total (sizeOfSecond+1)
			int c_previous = 0;
			int c_current = 0;
			for (int index = 0; index < (second.size() + 1); index++)
			{
				if (index != 0)
				{
					// c_i
					c_current = frequencyDigitSymbol(
							nextDigitIndex.getAndIncrement(), wordIndex);
					generateAndStoreCarries(index, first, second, c_previous,
							c_current, allMiddleVariableExpressions);
					c_previous = c_current;
				}

				//s_i
				int s_current = frequencyDigitSymbol(
						nextDigitIndex.getAndIncrement(), wordIndex);
				generateAndStoreSummations(index, first, second, c_current,
						s_current, allMiddleVariableExpressions);

				frequencySummationDigits.add(s_current);
			}

			// queue the new frequency summation digits for one synset of a current word
			frequencyDigitsQueue.offer(frequencySummationDigits);
			// then resort it by size
			Collections.sort(frequencyDigitsQueue, queueSizeSorter);
		}

		return allMiddleVariableExpressions;
	}

	private void generateAndStoreSummations(int index, IntList first,
			IntList second, int c_current, int s_current,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		if (index == 0)
		{
			// DO NOT use c_current since c_0 = '0'
			int x_0 = first.get(0);
			int y_0 = second.get(0);
			generateAndStoreFirstSummation(x_0, y_0, s_current,
					allMiddleVariableExpression);
		}
		else if (index < first.size())
		{
			Assert.isTrue(c_current != 0);
			int x_current = first.get(index);
			int y_current = second.get(index);
			generateAndStoreTwoAddendsSummation(x_current, y_current,
					c_current, s_current, allMiddleVariableExpression);
		}
		else if (index < second.size())
		{
			Assert.isTrue(c_current != 0);
			int y_current = second.get(index);
			generateAndStoreOneAddendSummation(y_current, c_current, s_current,
					allMiddleVariableExpression);
		}
		else
		{
			Assert.isTrue(c_current != 0);
			generateAndStoreLastSummation(c_current, s_current,
					allMiddleVariableExpression);
		}

	}

	/**
	 * s_0
	 */
	private void generateAndStoreFirstSummation(int x_0, int y_0, int s_0,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{

		int[] clause1 = new int[] { not(x_0), y_0 };
		Arrays.sort(clause1);

		int[] clause2 = new int[] { x_0, not(y_0) };
		Arrays.sort(clause2);

		allMiddleVariableExpression.put(s_0, new MiddleVariableExpression(
				clause1, clause2));
	}

	private void generateAndStoreTwoAddendsSummation(int x_current,
			int y_current, int c_current, int s_current,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		int[] clause1 = new int[] { not(x_current), not(y_current), c_current };
		Arrays.sort(clause1);

		int[] clause2 = new int[] { not(x_current), y_current, not(c_current) };
		Arrays.sort(clause2);

		int[] clause3 = new int[] { x_current, not(y_current), not(c_current) };
		Arrays.sort(clause3);

		int[] clause4 = new int[] { x_current, y_current, c_current };
		Arrays.sort(clause4);

		allMiddleVariableExpression
				.put(s_current, new MiddleVariableExpression(clause1, clause2,
						clause3, clause4));
	}

	private void generateAndStoreOneAddendSummation(int y_current,
			int c_current, int s_current,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		int[] clause1 = new int[] { not(y_current), c_current };
		Arrays.sort(clause1);

		int[] clause2 = new int[] { y_current, not(c_current) };
		Arrays.sort(clause2);

		allMiddleVariableExpression.put(s_current,
				new MiddleVariableExpression(clause1, clause2));
	}

	private void generateAndStoreLastSummation(int c_current, int s_current,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		// s_last = c_last
		MiddleVariableExpression expression = allMiddleVariableExpression
				.remove(c_current);
		Assert.notNull(expression, "The last carry must already be computed. ");
		allMiddleVariableExpression.put(s_current, expression);
	}

	//////////////////////////////////

	// For carries: 	  1, 2, 3, ..., sizeOfFirst ~ total sizeOfFirst
	// addendIndex:    0, 1, 2, 3, ..., ..., ..., sizeOfSecond
	private void generateAndStoreCarries(int index, IntList first,
			IntList second, int c_previous, int c_current,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		if (index == 1)
		{
			int x_0 = first.get(0);
			int y_0 = second.get(0);
			// DO NOT use c_previous here since c_0 = '0'!
			generateAndStoreFirstCarry(x_0, y_0, c_current,
					allMiddleVariableExpression);
		}
		else if (index <= first.size())
		{
			Assert.isTrue(c_previous != 0);
			int x_previous = first.get(index - 1);
			int y_previous = second.get(index - 1);

			generateAndStoreMiddleCarries(x_previous, y_previous, c_previous,
					c_current, allMiddleVariableExpression);
		}
		else
		{
			Assert.isTrue(c_previous != 0);
			int y_previous = second.get(index - 1);
			generateAndStoreLastCarry(y_previous, c_previous, c_current,
					allMiddleVariableExpression);
		}
	}

	private void generateAndStoreFirstCarry(int x_0, int y_0, int c_1,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		// c_previous/c_0 equals to '0', so there's no c_0 variable
		// c1 = x_0 AND y_0
		int[] clause = new int[] { x_0, y_0 };
		Arrays.sort(clause);

		allMiddleVariableExpression.put(c_1, new MiddleVariableExpression(
				clause));
	}

	private void generateAndStoreMiddleCarries(int x_previous, int y_previous,
			int c_previous, int c_current,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		int[] clause1 = new int[] { x_previous, y_previous };
		Arrays.sort(clause1);

		int[] clause2 = new int[] { x_previous, c_previous };
		Arrays.sort(clause2);

		int[] clause3 = new int[] { y_previous, c_previous };
		Arrays.sort(clause3);

		allMiddleVariableExpression.put(c_current,
				new MiddleVariableExpression(clause1, clause2, clause3));
	}

	/**
	 * Same as {@link #generateAndStoreFirstCarry(int, int, int, Map)}
	 */
	private void generateAndStoreLastCarry(int y_previous, int c_previous,
			int c_current,
			Map<Integer, MiddleVariableExpression> allMiddleVariableExpression)
	{
		int[] clause = new int[] { y_previous, c_previous };
		Arrays.sort(clause);

		allMiddleVariableExpression.put(c_current,
				new MiddleVariableExpression(clause));

	}

	////////////////////////////////////////////////////////////////////////////

	private Collection<int[]> generateCnfForSummationLessThanOrEqualsToValue(
			IntList finalFrequencySummationDigits, int value)
	{
		int totalSummationDigitsNumber = finalFrequencySummationDigits.size();
		// NOTICE! reverse order!
		String valueBinaryString = StringUtils.reverse(Integer
				.toBinaryString(value));
		int valueBinaryStringLength = valueBinaryString.length();
		Assert.isTrue(
				totalSummationDigitsNumber >= valueBinaryStringLength,
				"The number of total ["
						+ totalSummationDigitsNumber
						+ "] bits for summation must greater than or equals to the number of bits for value["
						+ value + "(" + Integer.toBinaryString(value) + ")]. ");

		Collection<int[]> greaterThanInCnf = generateCnfForSummationGreaterThanValue(
				finalFrequencySummationDigits, value);
		for (int[] eachClause : greaterThanInCnf)
		{
			for (int index = 0; index < eachClause.length; index++)
			{
				eachClause[index] = not(eachClause[index]);
			}
		}
		List<int[]> notGreaterThanInDnf = new ArrayList<int[]>(greaterThanInCnf);

		return convertDnfToCnf(notGreaterThanInDnf);

	}

	/**
	 *  -------------------
	 * |Step 5 in my report|
	 *  -------------------
	 *  
	 * @param finalFrequencySummationDigits
	 * @param value
	 * @return
	 */
	private Collection<int[]> generateCnfForSummationGreaterThanValue(
			IntList finalFrequencySummationDigits, int value)
	{
		int totalSummationDigitsNumber = finalFrequencySummationDigits.size();
		// NOTICE! reverse order!
		String valueBinaryString = StringUtils.reverse(Integer
				.toBinaryString(value));
		int valueBinaryStringLength = valueBinaryString.length();
		Assert.isTrue(
				totalSummationDigitsNumber >= valueBinaryStringLength,
				"The number of bits for summation["
						+ totalSummationDigitsNumber
						+ "]bits must greater than or equals to the number of bits for value["
						+ value + "]. ");

		ArrayList<IntList> allCnfClauses = new ArrayList<IntList>();

		// drop first '1's
		int index = 0;
		while (index < valueBinaryStringLength
				&& valueBinaryString.charAt(index) == '1')
		{
			index++;
		}
		ArrayIntList intList = new ArrayIntList();
		allCnfClauses.add(intList);
		////////////////////////////////////////////////////////////////////////

		for (; index < totalSummationDigitsNumber; index++)
		{
			if (index < valueBinaryStringLength
					&& valueBinaryString.charAt(index) == '1')
			{
				intList = new ArrayIntList();
				intList.add(finalFrequencySummationDigits.get(index));
				allCnfClauses.add(intList);
			}
			else
			{
				for (IntList eachClause : allCnfClauses)
				{
					eachClause.add(finalFrequencySummationDigits.get(index));
				}
			}
		}

		Set<int[]> result = new TreeSet<int[]>(new IntArrayComparator());
		int[] clauseArray = null;
		for (IntList clause : allCnfClauses)
		{
			clauseArray = clause.toArray();
			Arrays.sort(clauseArray);
			result.add(clauseArray);
		}

		return result;
	}

	public static void main(String[] args)
	{
		AddingFrequencyCnfGeneratorImpl impl = new AddingFrequencyCnfGeneratorImpl(
				null);
		IntList finalFrequencySummationDigits = new ArrayIntList();
		finalFrequencySummationDigits.add(0);
		finalFrequencySummationDigits.add(1);
		finalFrequencySummationDigits.add(2);
		finalFrequencySummationDigits.add(3);

		for (int index = 0; index < 16; index++)
		{
			Collection<int[]> result = impl
					.generateCnfForSummationGreaterThanValue(
							finalFrequencySummationDigits, index);
			System.out.print(index + ": ");
			for (int[] each : result)
			{
				System.out.print(Arrays.toString(each) + " /\\ ");
			}

			result = impl.generateCnfForSummationLessThanOrEqualsToValue(
					finalFrequencySummationDigits, index);
			System.out.print("		");
			for (int[] each : result)
			{
				System.out.print(Arrays.toString(each) + " \\/ ");
			}

			System.out.println();
		}

		System.out.println("==============================================");
		ArrayList<int[]> dnfs = new ArrayList<int[]>();
		dnfs.add(new int[] { 0 });
		dnfs.add(new int[] { 1 });
		dnfs.add(new int[] { 2 });
		dnfs.add(new int[] { 3 });
		List<int[]> result = impl.convertDnfToCnf(dnfs);
		for (int[] each : result)
		{
			System.out.println(Arrays.toString(each));
		}
	}
}
